In [1]:
import proveit
from proveit import defaults, ExprTuple, ExprRange
from proveit import k, m, s, t, U
from proveit.numbers import (
Mult, Exp, zero, one, two, subtract, exp2pi_i)
from proveit.linear_algebra import MatrixExp, TensorProd
from proveit.physics.quantum import var_ket_u, varphi
from proveit.physics.quantum.circuits import (
QcircuitEquiv, phase_kickbacks_on_register)
from proveit.physics.quantum.QPE import (
_s, _t, _ket_u, _U, _phase,
_s_in_nat_pos, _u_ket_register, _normalized_ket_u, _unitary_U, _phase_in_interval, _eigen_uu,
QPE1_def, _psi_t_def, _psi_t_ket_register)
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving _psi_t_output
Out[2]:
In [3]:
_psi_t_output
Out[3]:
In [4]:
defaults.assumptions = _psi_t_output.conditions
Out[4]:
defaults.assumptions: 
In [ ]:
We should automate the following so it isn't necessary.¶
In [5]:
_s_in_nat_pos
Out[5]:
In [6]:
from proveit.logic import InSet
from proveit.numbers import Natural, greater, greater_eq, zero, Neg
In [7]:
# greater_eq(_s, one).prove().derive_shifted(Neg(one))
In [8]:
# InSet(subtract(_s, one), Natural).prove()
In [9]:
# greater_eq(t, one).prove().derive_shifted(Neg(one))
In [10]:
tm1_in_N = InSet(subtract(t, one), Natural).prove()
Out[10]:
tm1_in_N: 
⊢ 
⊢ 
In [11]:
tm1_in_N.inner_expr().element.commute()
Out[11]:
In [ ]:
In [12]:
_psi_t_def
Out[12]:
In [13]:
_psi_t = _psi_t_def.instantiate()
Out[13]:
_psi_t: ⊢ 
⊢ 
In [14]:
_psi_t_ket_register
Out[14]:
In [15]:
_psi_t_ket_register.instantiate()
Out[15]:
In [ ]:
In [16]:
from proveit.logic import CartExp
from proveit.numbers import Complex
In [17]:
#InSet(_psi_t.rhs, CartExp(Complex, Exp(two, t))).prove()
In [18]:
from proveit import r
from proveit.numbers import NaturalPos
InSet(_psi_t.rhs.operands[0].body, CartExp(Complex, two)).prove(assumptions=[InSet(r, NaturalPos)])
Out[18]:
In [19]:
InSet(_psi_t.rhs.operands[0].body, CartExp(Complex, Exp(two, one))).prove(assumptions=[InSet(r, NaturalPos)])
Out[19]:
In [20]:
# InSet(_psi_t.rhs.operands[0].body.scaled, CartExp(Complex, two)).prove(assumptions=[InSet(r, NaturalPos)])
In [21]:
# from proveit.linear_algebra import TensorProd
# InSet(TensorProd(_psi_t.rhs.operands[0].body, _psi_t.rhs.operands[0].body), CartExp(Complex, Exp(two, two))).prove()
In [ ]:
In [22]:
target_circuit = _psi_t_output.instance_expr.lhs.operand
Out[22]:
target_circuit: 
In [23]:
QPE1_def
Out[23]:
In [24]:
QPE1_inst = QPE1_def.instantiate({s:_s, U:_U})
Out[24]:
QPE1_inst: ⊢ 
⊢ 
In [25]:
phase_kickbacks_on_register
Out[25]:
In [26]:
Uexponentials = ExprTuple(ExprRange(k, MatrixExp(_U, Exp(two, k)),
subtract(t, one), zero, order='decreasing'))
Out[26]:
Uexponentials: 
In [ ]:
We should automate the following so it isn't necessary.¶
In [27]:
Neg(subtract(t, one)).simplification()
Out[27]:
In [28]:
t_gt_0 = greater(t, zero).prove()
Out[28]:
t_gt_0: ⊢ 
⊢ 
In [29]:
from proveit.numbers import Less
Less(Neg(one), zero).prove()
Out[29]:
In [30]:
nt_lt_0 = t_gt_0.left_mult_both_sides(Neg(one))
Out[30]:
nt_lt_0: ⊢ 
⊢ 
In [31]:
nt_lt_0.derive_shifted(one)
Out[31]:
In [32]:
t_geq_1 = greater_eq(t, one).prove()
Out[32]:
t_geq_1: ⊢ 
⊢ 
In [33]:
nt_leq_1 = t_geq_1.left_mult_both_sides(Neg(one))
Out[33]:
nt_leq_1: ⊢ 
⊢ 
In [34]:
nt_leq_1.derive_shifted(two)
Out[34]:
In [35]:
nt_lt_0.derive_shifted(one)
Out[35]:
In [36]:
from proveit.numbers import Add
Add(t, one).commutation()
Out[36]:
In [37]:
Add(t, two).commutation()
Out[37]:
In [38]:
from proveit.numbers import Interval
tmp_assumptions = defaults.assumptions+(InSet(k, Interval(Add(Neg(t), one), zero)),)
k_gt_ntp1 = greater_eq(k, Add(Neg(t), one)).prove(
assumptions=tmp_assumptions)
Out[38]:
k_gt_ntp1: , 
⊢ 
, 
⊢ 
In [39]:
from proveit.numbers import Integer
Add(k, t).deduce_bound(k_gt_ntp1, assumptions=tmp_assumptions)
Out[39]:
, ⊢ 
In [40]:
greater(Add(k, t), zero).prove(assumptions=tmp_assumptions)
Out[40]:
, ⊢ 
In [41]:
InSet(Add(k, t), Integer).prove(assumptions=tmp_assumptions)
Out[41]:
, ⊢ 
In [42]:
InSet(Add(k, t), Natural).prove(assumptions=tmp_assumptions).generalize(
k, conditions=[InSet(k, Interval(Add(Neg(t), one), zero))])
Out[42]:
In [43]:
subtract(one, Add(Neg(t), two)).simplification()
Out[43]:
In [ ]:
In [44]:
from proveit.logic import And, InSet
And(ExprRange(k, InSet(MatrixExp(_U, Exp(two, k)), _unitary_U.domain),
subtract(t, one), zero, order='decreasing')).conclude_over_expr_range()
Out[44]:
In [45]:
phases = ExprTuple(ExprRange(k, Mult(Exp(two, k), _phase),
subtract(t, one), zero, order='decreasing'))
Out[45]:
phases: 
In [ ]:
In [46]:
kickbacks = phase_kickbacks_on_register.instantiate(
{m:_s, U:Uexponentials, var_ket_u:_ket_u, varphi:phases})
Out[46]:
kickbacks: ⊢ 
⊢ 
In [47]:
kickbacks_with_QPE1 = QPE1_inst.sub_left_side_into(
kickbacks.inner_expr().lhs.operand)
Out[47]:
kickbacks_with_QPE1: ⊢ 
⊢ 
For psi_t_tensor_u_expansion to simplify properly, we need to specify this default vector-space field, but we should be able to automate this in the future:
In [48]:
from proveit.linear_algebra import VecSpaces
VecSpaces.default_field = Complex
Out[48]:
VecSpaces.default_field: 
In [49]:
psi_t_tensor_u__expansion = _psi_t.substitution(TensorProd(_psi_t.lhs, _ket_u))
Out[49]:
psi_t_tensor_u__expansion: ⊢ 
⊢ 
In [ ]:
We should automate the following so it isn't necessary.¶
In [50]:
from proveit._core_.expression.label.var import dummy_var
assumptions = defaults.assumptions + (InSet(dummy_var(0), Interval(Add(Neg(t), one), zero)),)
Out[50]:
assumptions: 
In [51]:
Add(dummy_var(0), t).deduce_bound(assumptions[1].derive_element_lower_bound(
assumptions=assumptions).reversed(), assumptions=assumptions)
Out[51]:
, 
⊢ 
In [52]:
Add(dummy_var(0), t).deduce_in_number_set(NaturalPos, assumptions=assumptions)
Out[52]:
, ⊢ 
In [ ]:
In [53]:
output_consolidation = kickbacks_with_QPE1.lhs.operand.output_consolidation(
replacements=[psi_t_tensor_u__expansion.derive_reversed()])
Out[53]:
output_consolidation: ⊢ 
⊢ 
In [54]:
output_consolidation_from_desired = _psi_t_output.instance_expr.lhs.operand.output_consolidation()
Out[54]:
output_consolidation_from_desired: ⊢ 
⊢ 
In [55]:
equiv = output_consolidation.apply_transitivity(
output_consolidation_from_desired, assumptions=defaults.assumptions + (InSet(_psi_t.rhs, CartExp(Complex, Exp(two, t))),))
Out[55]:
equiv: ⊢ 
⊢ 
In [56]:
equiv.sub_right_side_into(kickbacks_with_QPE1)
Out[56]:
In [57]:
%qed
Out[57]:
| step type | requirements | statement | ||
|---|---|---|---|---|
| 0 | generalization | 1 | ⊢ | |
| 1 | instantiation | 4, 2, 3 | ⊢  | |
 :  ,  :  ,  : | ||||
| 2 | instantiation | 4, 5, 6 | ⊢ | |
: , :  , : | ||||
| 3 | instantiation | 7, 8, 9 | ⊢ | |
: , :  ,  : | ||||
| 4 | conjecture | ⊢  | ||
| proveit.physics.quantum.circuits.rhs_prob_via_equiv | ||||
| 5 | instantiation | 10, 494, 689, 11, 12, 338, 13, 14, 15, 680, 656, 16, 17* | ⊢ | |
 :  ,  : ,  : ,  : ,  : | ||||
| 6 | modus ponens | 18, 19 | ⊢  | |
| 7 | conjecture | ⊢  | ||
| proveit.physics.quantum.circuits.equiv_transitivity | ||||
| 8 | modus ponens | 20, 21 | ⊢  | |
| 9 | instantiation | 34, 22 | ⊢  | |
| : , : | ||||
| 10 | conjecture | ⊢  | ||
| proveit.physics.quantum.circuits.phase_kickbacks_on_register | ||||
| 11 | instantiation | 584, 23, 467 | ⊢  | |
 :  ,  : ,  :  | ||||
| 12 | modus ponens | 24, 25 | ⊢  | |
| 13 | axiom | ⊢  | ||
| proveit.physics.quantum.QPE._normalized_ket_u | ||||
| 14 | instantiation | 584, 26, 467 | ⊢  | |
:  , : , : | ||||
| 15 | modus ponens | 27, 28 | ⊢  | |
| 16 | instantiation | 263, 679, 264, 75, 76, 77* | ⊢  | |
 :  ,  :  ,  :  ,  :  ,  :  ,  : | ||||
| 17 | instantiation | 29, 614, 664, 682, 30, 31, 615, 602, 594, 595, 32, 597 | ,  ⊢  | |
:  , :  , : , :  ,  :  ,  :  | ||||
| 18 | instantiation | 51, 610, 527, 33 | ⊢  | |
: , : , : , : , :  , :  , :  ,  :  | ||||
| 19 | instantiation | 34, 35 | ⊢  | |
:  , :  | ||||
| 20 | instantiation | 51, 664, 610, 682, 52, 615 | ⊢  | |
: , : , : , : , :  , : , : , :  | ||||
| 21 | instantiation | 578, 36, 37 | ⊢  | |
 :  , :  , :  | ||||
| 22 | modus ponens | 38, 39 | ⊢  | |
| 23 | instantiation | 578, 40, 528 | ⊢  | |
 :  , :  , : | ||||
| 24 | instantiation | 471, 676, 677, 472 | ⊢  | |
: , : ,  :  , : | ||||
| 25 | generalization | 41 | ⊢  | |
| 26 | instantiation | 578, 42, 528 | ⊢  | |
:  , : , : | ||||
| 27 | instantiation | 471, 676, 677, 472 | ⊢  | |
: , : ,  :  , : | ||||
| 28 | generalization | 43 | ⊢  | |
| 29 | conjecture | ⊢  | ||
| proveit.numbers.multiplication.disassociation | ||||
| 30 | instantiation | 632 | ⊢  | |
: , :  , :  | ||||
| 31 | instantiation | 631 | ⊢  | |
:  , : | ||||
| 32 | instantiation | 685, 635, 44 | , ⊢  | |
:  , : , : | ||||
| 33 | instantiation | 584, 45, 467 | ⊢  | |
:  , : , : | ||||
| 34 | conjecture | ⊢  | ||
| proveit.physics.quantum.circuits.equiv_reflexivity | ||||
| 35 | instantiation | 46, 494, 689, 64 | ⊢ | |
| : , : , : | ||||
| 36 | instantiation | 578, 47, 48 | ⊢  | |
 :  , :  , : | ||||
| 37 | instantiation | 238, 527, 72, 49, 50 | ⊢  | |
 : ,  :  , :  , :  | ||||
| 38 | instantiation | 51, 664, 610, 682, 52, 615 | ⊢  | |
: , : , : , : , : , :  , : , : | ||||
| 39 | instantiation | 89, 666, 53, 689, 494, 54, 55, 338, 56, 57, 58, 59, 60, 579, 417, 682, 527, 103, 61, 605* | ⊢  | |
: , :  , :  ,  :  ,  : ,  : | ||||
| 40 | instantiation | 508, 509 | ⊢  | |
 :  , : , : | ||||
| 41 | instantiation | 62, 63, 435, 64 | , ⊢ | |
:  , :  , : | ||||
| 42 | instantiation | 508, 509 | ⊢  | |
:  , : , : | ||||
| 43 | instantiation | 65, 123, 627, 66 | , ⊢ | |
: ,  : , : , : | ||||
| 44 | instantiation | 685, 652, 67 | , ⊢  | |
:  , : , : | ||||
| 45 | instantiation | 578, 68, 528 | ⊢  | |
:  , : , : | ||||
| 46 | axiom | ⊢  | ||
| proveit.physics.quantum.QPE.QPE1_def | ||||
| 47 | instantiation | 578, 69, 70 | ⊢  | |
:  , :  , :  | ||||
| 48 | instantiation | 238, 527, 71, 72, 73 | ⊢  | |
: , : , :  , : | ||||
| 49 | instantiation | 74, 527 | ⊢  | |
: , :  | ||||
| 50 | instantiation | 263, 679, 264, 75, 76, 77* | ⊢  | |
 :  , : , : , : , : , : | ||||
| 51 | conjecture | ⊢  | ||
| proveit.physics.quantum.circuits.circuit_equiv_temporal_sub | ||||
| 52 | instantiation | 631 | ⊢  | |
:  , :  | ||||
| 53 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 54 | instantiation | 631 | ⊢  | |
:  , : | ||||
| 55 | instantiation | 78, 689 | ⊢  | |
| : | ||||
| 56 | instantiation | 584, 79, 80 | ⊢  | |
:  , : , :  | ||||
| 57 | instantiation | 492, 81 | ⊢  | |
:  , : | ||||
| 58 | instantiation | 631 | ⊢  | |
: , :  | ||||
| 59 | instantiation | 492, 82 | ⊢  | |
: , :  | ||||
| 60 | instantiation | 584, 83, 84 | ⊢  | |
:  , : , :  | ||||
| 61 | instantiation | 186, 614, 85, 189, 86, 192 | ⊢  | |
: , :  | ||||
| 62 | conjecture | ⊢  | ||
| proveit.linear_algebra.matrices.exponentiation.U_closure | ||||
| 63 | instantiation | 663, 664, 87 | , ⊢  | |
: , :  | ||||
| 64 | axiom | ⊢  | ||
| proveit.physics.quantum.QPE._unitary_U | ||||
| 65 | conjecture | ⊢  | ||
| proveit.linear_algebra.matrices.exponentiation.unital2pi_eigen_exp_application | ||||
| 66 | axiom | ⊢  | ||
| proveit.physics.quantum.QPE._eigen_uu | ||||
| 67 | instantiation | 685, 655, 88 | , ⊢  | |
:  , : , : | ||||
| 68 | instantiation | 508, 509 | ⊢  | |
:  , : , : | ||||
| 69 | instantiation | 89, 364, 90, 687, 91, 494, 92, 93, 94, 338, 95, 96, 97, 98, 99, 100, 101, 579, 176, 682, 102, 103, 104, 605, 327*, 105*, 106* | ⊢  | |
:  , :  , :  , :  ,  :  ,  :  | ||||
| 70 | instantiation | 238, 527, 107, 108, 109, 110* | ⊢  | |
: ,  :  , :  , :  | ||||
| 71 | instantiation | 584, 111, 467 | ⊢  | |
:  , : , : | ||||
| 72 | instantiation | 584, 112, 467 | ⊢  | |
:  , : , : | ||||
| 73 | instantiation | 282, 283, 284, 371* | ⊢  | |
:  , : , :  , : | ||||
| 74 | conjecture | ⊢  | ||
| proveit.core_expr_types.tuples.range_from1_len_typical_eq | ||||
| 75 | instantiation | 492, 113 | ⊢  | |
:  , : | ||||
| 76 | instantiation | 492, 114 | ⊢  | |
:  , : | ||||
| 77 | instantiation | 584, 115, 116 | ,  ⊢  | |
:  , :  , : | ||||
| 78 | conjecture | ⊢  | ||
| proveit.physics.quantum.QPE._psi_t_ket_register | ||||
| 79 | instantiation | 117 | ⊢  | |
| : , : , : | ||||
| 80 | instantiation | 492, 118 | ⊢  | |
| : , : | ||||
| 81 | instantiation | 218, 119, 605 | ⊢  | |
 :  , : , : | ||||
| 82 | instantiation | 270, 119, 417 | ⊢  | |
| : , : , : | ||||
| 83 | instantiation | 120 | ⊢  | |
| : , : | ||||
| 84 | instantiation | 492, 121 | ⊢  | |
| : , : | ||||
| 85 | instantiation | 632 | ⊢  | |
:  , :  , :  | ||||
| 86 | instantiation | 492, 481 | ⊢ | |
:  , : | ||||
| 87 | instantiation | 667, 122 | , ⊢  | |
| : | ||||
| 88 | instantiation | 685, 686, 123 | , ⊢  | |
:  , : , : | ||||
| 89 | conjecture | ⊢  | ||
| proveit.physics.quantum.circuits.output_consolidation | ||||
| 90 | instantiation | 584, 124, 134 | ⊢  | |
:  , : , :  | ||||
| 91 | instantiation | 468, 654, 677, 687, 279 | ⊢  | |
: , : , :  | ||||
| 92 | instantiation | 584, 125, 134 | ⊢  | |
:  , : , : | ||||
| 93 | instantiation | 526, 126, 209 | ⊢  | |
:  , :  , :  | ||||
| 94 | modus ponens | 127, 128 | ⊢  | |
| 95 | instantiation | 584, 129, 130 | ⊢  | |
:  , :  , :  | ||||
| 96 | instantiation | 492, 131 | ⊢  | |
:  , :  | ||||
| 97 | instantiation | 492, 132 | ⊢  | |
| : , : | ||||
| 98 | instantiation | 584, 133, 134 | ⊢  | |
:  , : , : | ||||
| 99 | instantiation | 492, 135 | ⊢  | |
: , :  | ||||
| 100 | instantiation | 492, 136 | ⊢  | |
| : , : | ||||
| 101 | instantiation | 584, 137, 138 | ⊢  | |
:  , : , :  | ||||
| 102 | modus ponens | 139, 140 | ⊢  | |
| 103 | instantiation | 685, 543, 141 | ⊢  | |
: , :  , : | ||||
| 104 | instantiation | 142, 664, 358, 610, 143, 426, 144, 145 | ⊢  | |
: , :  , : , :  , :  , :  | ||||
| 105 | instantiation | 584, 146, 147 | ⊢  | |
:  , :  , :  | ||||
| 106 | instantiation | 584, 148, 198 | ⊢  | |
:  , :  , :  | ||||
| 107 | instantiation | 584, 149, 467 | ⊢  | |
:  , : , : | ||||
| 108 | instantiation | 584, 150, 467 | ⊢  | |
:  , : , : | ||||
| 109 | instantiation | 282, 283, 284, 151* | ⊢  | |
:  , : , : , : | ||||
| 110 | instantiation | 245, 152 | , ⊢  | |
 :  , :  | ||||
| 111 | instantiation | 328, 666, 153, 330, 344, 331, 358, 332* | ⊢  | |
: ,  :  , :  , :  | ||||
| 112 | instantiation | 578, 154, 528 | ⊢  | |
:  , : , : | ||||
| 113 | instantiation | 584, 155, 371 | ⊢  | |
: , :  , : | ||||
| 114 | instantiation | 584, 156, 481 | ⊢  | |
| : , : , : | ||||
| 115 | instantiation | 609, 682, 664, 610, 615, 157, 158, 582, 617 | , ⊢  | |
: , : , : , : , :  , :  | ||||
| 116 | instantiation | 587, 617, 158 | , ⊢  | |
| : , : | ||||
| 117 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.tuple_len_3 | ||||
| 118 | instantiation | 578, 159, 248 | ⊢  | |
:  , :  , : | ||||
| 119 | instantiation | 526, 664, 160 | ⊢  | |
:  , :  , : | ||||
| 120 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.tuple_len_2 | ||||
| 121 | instantiation | 578, 161, 249 | ⊢  | |
:  , :  , : | ||||
| 122 | instantiation | 669, 453, 162 | , ⊢  | |
| : | ||||
| 123 | instantiation | 663, 664, 163 | , ⊢  | |
: , :  | ||||
| 124 | instantiation | 328, 210, 164, 180, 213, 331, 358, 181* | ⊢  | |
: , :  , :  , :  | ||||
| 125 | instantiation | 328, 210, 165, 180, 213, 331, 358, 181* | ⊢  | |
: , :  , : , : | ||||
| 126 | instantiation | 532, 533, 496, 166 | ⊢  | |
 : ,  : , :  , :  | ||||
| 127 | instantiation | 471, 654, 677, 279 | ⊢  | |
: , : , :  , : | ||||
| 128 | generalization | 167 | ⊢  | |
| 129 | instantiation | 584, 168, 169 | ⊢  | |
: , :  , : | ||||
| 130 | instantiation | 492, 170 | ⊢  | |
| : , : | ||||
| 131 | instantiation | 218, 175, 605 | ⊢  | |
| : , : , : | ||||
| 132 | instantiation | 238, 527, 222, 171, 172 | ⊢  | |
: , :  , :  , :  | ||||
| 133 | instantiation | 328, 210, 173, 180, 213, 331, 358, 181* | ⊢  | |
: , :  , : , : | ||||
| 134 | instantiation | 492, 174 | ⊢  | |
| : , : | ||||
| 135 | instantiation | 270, 175, 176 | ⊢  | |
| : , : , : | ||||
| 136 | instantiation | 584, 177, 178 | ⊢  | |
: , :  , : | ||||
| 137 | instantiation | 328, 210, 179, 180, 213, 331, 358, 181* | ⊢  | |
: , :  , : , : | ||||
| 138 | instantiation | 492, 182 | ⊢  | |
| : , : | ||||
| 139 | instantiation | 471, 676, 677, 472 | ⊢  | |
: , : , :  , : | ||||
| 140 | generalization | 183 | ⊢  | |
| 141 | instantiation | 406, 689, 494 | ⊢  | |
| : , : | ||||
| 142 | conjecture | ⊢  | ||
| proveit.logic.booleans.conjunction.disassociate | ||||
| 143 | instantiation | 631 | ⊢  | |
: , :  | ||||
| 144 | instantiation | 584, 184, 185 | ⊢  | |
:  , :  , :  | ||||
| 145 | instantiation | 186, 187, 188, 189, 190, 191, 192 | ⊢  | |
:  , :  | ||||
| 146 | instantiation | 576, 193 | ⊢  | |
:  , : , :  | ||||
| 147 | instantiation | 492, 194 | ⊢  | |
| : , : | ||||
| 148 | instantiation | 576, 605 | ⊢  | |
:  , :  , : | ||||
| 149 | instantiation | 328, 666, 195, 330, 344, 331, 358, 332* | ⊢  | |
: , :  , : , : | ||||
| 150 | instantiation | 578, 196, 528 | ⊢  | |
:  , : , : | ||||
| 151 | instantiation | 584, 197, 198 | ⊢  | |
:  , : , : | ||||
| 152 | instantiation | 199, 200, 201 | , ⊢ | |
| : | ||||
| 153 | instantiation | 631 | ⊢  | |
 :  ,  : | ||||
| 154 | instantiation | 508, 509 | ⊢  | |
 :  , : , : | ||||
| 155 | instantiation | 576, 583 | ⊢  | |
:  , :  , : | ||||
| 156 | instantiation | 576, 583 | ⊢  | |
:  , : , : | ||||
| 157 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 158 | instantiation | 685, 635, 202 | , ⊢  | |
| : , : , : | ||||
| 159 | instantiation | 508, 203 | ⊢  | |
| : , : , : | ||||
| 160 | instantiation | 584, 204, 439 | ⊢  | |
: , :  , : | ||||
| 161 | instantiation | 508, 205 | ⊢  | |
| : , : , : | ||||
| 162 | instantiation | 673, 676, 677, 483 | , ⊢  | |
| : , : , : | ||||
| 163 | instantiation | 667, 206 | , ⊢  | |
| : | ||||
| 164 | instantiation | 632 | ⊢  | |
: ,  : ,  : | ||||
| 165 | instantiation | 632 | ⊢  | |
:  , :  , : | ||||
| 166 | instantiation | 514, 533, 515, 207 | ⊢  | |
: , : , :  , :  | ||||
| 167 | instantiation | 526, 208, 209 | ,  ⊢ | |
:  , : , : | ||||
| 168 | instantiation | 328, 210, 211, 212, 213, 331, 509, 214* | ⊢  | |
: , :  , :  , : | ||||
| 169 | instantiation | 492, 215 | ⊢  | |
| : , : | ||||
| 170 | instantiation | 578, 216, 304 | ⊢  | |
:  , :  , : | ||||
| 171 | instantiation | 584, 217, 467 | ⊢  | |
:  , : , : | ||||
| 172 | instantiation | 218, 283, 353, 371* | ⊢  | |
| : , : , : | ||||
| 173 | instantiation | 632 | ⊢  | |
 : ,  : ,  : | ||||
| 174 | instantiation | 510, 321 | ⊢  | |
| : , : | ||||
| 175 | instantiation | 526, 321, 219 | ⊢  | |
: , :  , : | ||||
| 176 | instantiation | 584, 220, 221 | ⊢  | |
:  , :  , : | ||||
| 177 | instantiation | 238, 527, 222, 224, 223 | ⊢  | |
: , : , : , :  | ||||
| 178 | instantiation | 238, 527, 224, 225, 226 | ⊢  | |
: , : , : , :  | ||||
| 179 | instantiation | 632 | ⊢  | |
: , :  , : | ||||
| 180 | instantiation | 632 | ⊢  | |
| : , : , : | ||||
| 181 | instantiation | 584, 227, 228 | ⊢  | |
:  , :  , : | ||||
| 182 | instantiation | 578, 229, 322 | ⊢  | |
:  , :  , : | ||||
| 183 | instantiation | 553, 230, 231 | , ⊢  | |
:  | ||||
| 184 | instantiation | 578, 232, 426 | ⊢  | |
:  , : , : | ||||
| 185 | instantiation | 492, 233 | ⊢  | |
| : , : | ||||
| 186 | conjecture | ⊢  | ||
| proveit.logic.booleans.conjunction.and_if_all | ||||
| 187 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.nat4 | ||||
| 188 | instantiation | 234 | ⊢  | |
: , : , :  ,  : | ||||
| 189 | instantiation | 237 | ⊢ | |
| : | ||||
| 190 | instantiation | 492, 605 | ⊢ | |
| : , : | ||||
| 191 | modus ponens | 235, 236 | ⊢ | |
| 192 | instantiation | 237 | ⊢ | |
| : | ||||
| 193 | instantiation | 238, 527, 239, 385, 240 | ⊢  | |
: , :  , :  , :  | ||||
| 194 | instantiation | 576, 241, 242* | ⊢ | |
:  , : , :  | ||||
| 195 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 196 | instantiation | 508, 509 | ⊢  | |
:  , : , : | ||||
| 197 | instantiation | 422, 614, 243, 244, 371, 562 | ⊢  | |
: ,  :  , :  , :  | ||||
| 198 | instantiation | 245, 687 | ⊢  | |
| : , : | ||||
| 199 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.integers.pos_int_is_natural_pos | ||||
| 200 | instantiation | 678, 670, 656 | , ⊢  | |
| : , : | ||||
| 201 | instantiation | 323, 324, 246 | , ⊢  | |
| : , : , : | ||||
| 202 | instantiation | 685, 652, 247 | , ⊢  | |
| : , : , : | ||||
| 203 | instantiation | 526, 614, 248 | ⊢  | |
| : , : , : | ||||
| 204 | instantiation | 576, 407 | ⊢  | |
:  , :  , : | ||||
| 205 | instantiation | 526, 664, 249 | ⊢  | |
| : , : , : | ||||
| 206 | instantiation | 669, 250, 251 | , ⊢  | |
| : | ||||
| 207 | instantiation | 532, 533, 252, 535 | ⊢  | |
: , : , :  , :  | ||||
| 208 | instantiation | 532, 533, 496, 253 | , ⊢  | |
: , : , : , :  | ||||
| 209 | instantiation | 576, 254 | ⊢  | |
:  , :  , : | ||||
| 210 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.posnat3 | ||||
| 211 | instantiation | 632 | ⊢  | |
| : , : , : | ||||
| 212 | instantiation | 632 | ⊢  | |
| : , : , : | ||||
| 213 | instantiation | 632 | ⊢  | |
| : , : , : | ||||
| 214 | instantiation | 584, 255, 256 | ⊢  | |
:  , :  , : | ||||
| 215 | instantiation | 606, 617, 602 | ⊢  | |
| : , : | ||||
| 216 | instantiation | 508, 257 | ⊢  | |
| : , : , : | ||||
| 217 | instantiation | 328, 666, 258, 330, 344, 331, 358, 332* | ⊢  | |
: , :  , : , : | ||||
| 218 | conjecture | ⊢  | ||
| proveit.core_expr_types.tuples.partition_front | ||||
| 219 | instantiation | 584, 259, 260 | ⊢  | |
: , :  , : | ||||
| 220 | instantiation | 609, 682, 664, 610, 615, 477, 617, 619, 618 | ⊢  | |
: , : , : , : , :  , :  | ||||
| 221 | instantiation | 261, 619, 617 | ⊢  | |
| : , : | ||||
| 222 | instantiation | 584, 262, 467 | ⊢  | |
:  , : , : | ||||
| 223 | instantiation | 263, 571, 264, 265, 266, 267* | ⊢  | |
: , :  , : , : , : , : | ||||
| 224 | instantiation | 584, 268, 467 | ⊢  | |
:  , : , : | ||||
| 225 | instantiation | 584, 269, 467 | ⊢  | |
:  , : , : | ||||
| 226 | instantiation | 270, 271, 579, 272* | ⊢  | |
| : , : , : | ||||
| 227 | instantiation | 422, 614, 273, 274, 425, 426 | ⊢  | |
: , :  , :  , :  | ||||
| 228 | instantiation | 584, 275, 276 | ⊢  | |
: , :  , : | ||||
| 229 | instantiation | 508, 277 | ⊢  | |
| : , : , : | ||||
| 230 | instantiation | 678, 453, 656 | , ⊢ | |
| : , : | ||||
| 231 | instantiation | 511, 278 | , ⊢  | |
| : , : | ||||
| 232 | instantiation | 508, 358 | ⊢  | |
:  , : , : | ||||
| 233 | instantiation | 510, 536 | ⊢  | |
| : , : | ||||
| 234 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.tuple_len_4_typical_eq | ||||
| 235 | instantiation | 471, 654, 677, 279 | ⊢  | |
| : , : , : , : | ||||
| 236 | generalization | 280 | ⊢  | |
| 237 | axiom | ⊢  | ||
| proveit.logic.equality.equals_reflexivity | ||||
| 238 | conjecture | ⊢  | ||
| proveit.core_expr_types.operations.operands_substitution_via_tuple | ||||
| 239 | instantiation | 584, 281, 467 | ⊢  | |
:  , : , : | ||||
| 240 | instantiation | 282, 283, 284, 562* | ⊢  | |
| : , : , : , : | ||||
| 241 | instantiation | 285, 689 | ⊢ | |
| : | ||||
| 242 | modus ponens | 286, 287 | ⊢  | |
| 243 | instantiation | 632 | ⊢  | |
: , : , :  | ||||
| 244 | instantiation | 632 | ⊢  | |
| : , : , : | ||||
| 245 | conjecture | ⊢  | ||
| proveit.physics.quantum.circuits.unary_multi_output_reduction | ||||
| 246 | instantiation | 367, 633, 368, 288, 289, 371* | , ⊢  | |
| : , : , : | ||||
| 247 | instantiation | 685, 655, 290 | , ⊢  | |
| : , : , : | ||||
| 248 | instantiation | 584, 291, 292 | ⊢  | |
: , :  , : | ||||
| 249 | instantiation | 584, 293, 294 | ⊢  | |
: , :  , : | ||||
| 250 | instantiation | 685, 672, 295 | , ⊢  | |
:  , : , : | ||||
| 251 | instantiation | 673, 676, 677, 295 | , ⊢  | |
| : , : , : | ||||
| 252 | instantiation | 685, 551, 296 | ⊢  | |
:  , : , : | ||||
| 253 | instantiation | 514, 533, 515, 297 | , ⊢  | |
: , : , : , :  | ||||
| 254 | instantiation | 298, 602 | ⊢  | |
| : | ||||
| 255 | instantiation | 422, 614, 299, 300, 425, 528 | ⊢  | |
: , : , :  , :  | ||||
| 256 | instantiation | 584, 301, 302 | ⊢  | |
: , :  , : | ||||
| 257 | instantiation | 526, 303, 304 | ⊢  | |
| : , : , : | ||||
| 258 | instantiation | 631 | ⊢  | |
: ,  :  | ||||
| 259 | instantiation | 576, 407 | ⊢  | |
:  , : , : | ||||
| 260 | instantiation | 584, 305, 306 | ⊢  | |
: , :  , : | ||||
| 261 | conjecture | ⊢  | ||
| proveit.numbers.addition.subtraction.add_cancel_triple_23 | ||||
| 262 | instantiation | 578, 307, 528 | ⊢  | |
:  , : , : | ||||
| 263 | conjecture | ⊢  | ||
| proveit.core_expr_types.tuples.shift_equivalence | ||||
| 264 | instantiation | 526, 527, 308 | ⊢  | |
: , :  , : | ||||
| 265 | instantiation | 492, 309 | ⊢  | |
:  , : | ||||
| 266 | instantiation | 492, 310 | ⊢  | |
:  , : | ||||
| 267 | instantiation | 609, 682, 664, 610, 615, 311, 312, 618, 617 | ,  ⊢  | |
: , : , : , : , :  , : | ||||
| 268 | instantiation | 578, 313, 401 | ⊢  | |
:  , :  , : | ||||
| 269 | instantiation | 314, 315, 316* | ⊢  | |
:  , : , : , : | ||||
| 270 | conjecture | ⊢  | ||
| proveit.core_expr_types.tuples.partition_back | ||||
| 271 | instantiation | 526, 317, 318 | ⊢  | |
: , :  , :  | ||||
| 272 | instantiation | 319, 619, 617 | ⊢  | |
| : , : | ||||
| 273 | instantiation | 632 | ⊢  | |
:  , : , : | ||||
| 274 | instantiation | 632 | ⊢  | |
| : , : , : | ||||
| 275 | instantiation | 609, 610, 664, 611, 619, 617, 618 | ⊢  | |
: , : , : , :  , :  , : | ||||
| 276 | instantiation | 320, 682, 610, 615, 619, 617 | ⊢  | |
| : , : , : , : , : , : , : | ||||
| 277 | instantiation | 526, 321, 322 | ⊢  | |
| : , : , : | ||||
| 278 | instantiation | 323, 324, 325 | , ⊢  | |
| : , : , : | ||||
| 279 | instantiation | 526, 326, 605 | ⊢  | |
:  , : , : | ||||
| 280 | instantiation | 492, 327 | ,  ⊢ | |
:  , : | ||||
| 281 | instantiation | 328, 666, 329, 330, 344, 331, 358, 332* | ⊢  | |
: , :  , : , : | ||||
| 282 | conjecture | ⊢  | ||
| proveit.core_expr_types.tuples.merge_front | ||||
| 283 | instantiation | 526, 536, 333 | ⊢  | |
: , :  , : | ||||
| 284 | instantiation | 492, 353 | ⊢  | |
:  , : | ||||
| 285 | axiom | ⊢  | ||
| proveit.physics.quantum.QPE._psi_t_def | ||||
| 286 | instantiation | 334, 682, 509, 610, 335, 615, 528, 385 | ⊢  | |
: , : , : , : , :  , : , : , :  | ||||
| 287 | instantiation | 384, 666, 381, 382, 383, 336, 337, 338 | ⊢  | |
: , : , :  , :  | ||||
| 288 | instantiation | 685, 652, 339 | , ⊢  | |
| : , : , : | ||||
| 289 | instantiation | 410, 676, 677, 674 | , ⊢  | |
| : , : , : | ||||
| 290 | instantiation | 685, 340, 341 | , ⊢ | |
:  , : , : | ||||
| 291 | instantiation | 576, 407 | ⊢  | |
:  , : , : | ||||
| 292 | instantiation | 540, 682, 664, 610, 615, 342, 602, 612, 619, 343* | ⊢  | |
: , : , : , : , :  , : | ||||
| 293 | instantiation | 576, 407 | ⊢  | |
:  , : , : | ||||
| 294 | instantiation | 540, 682, 664, 610, 615, 344, 619, 612, 345* | ⊢  | |
| : , : , : , : , : , : | ||||
| 295 | assumption | ⊢ | ||
| 296 | instantiation | 568, 569, 346 | ⊢  | |
:  , :  | ||||
| 297 | instantiation | 532, 533, 347, 535 | , ⊢  | |
: , : , :  , : | ||||
| 298 | conjecture | ⊢  | ||
| proveit.numbers.exponentiation.complex_x_to_first_power_is_x | ||||
| 299 | instantiation | 632 | ⊢  | |
| : , : , : | ||||
| 300 | instantiation | 632 | ⊢  | |
| : , : , : | ||||
| 301 | instantiation | 558, 610, 682, 615, 619, 617 | ⊢  | |
| : , : , : , : , : , : , : | ||||
| 302 | instantiation | 540, 682, 664, 610, 615, 445, 619, 617, 603* | ⊢  | |
: , : , : , : , :  , : | ||||
| 303 | instantiation | 685, 543, 348 | ⊢  | |
| : , : , : | ||||
| 304 | instantiation | 584, 349, 350 | ⊢  | |
: , :  , : | ||||
| 305 | instantiation | 609, 682, 664, 610, 615, 477, 617, 619, 612 | ⊢  | |
: , : , : , : , : , :  | ||||
| 306 | instantiation | 613, 664, 682, 477, 615, 617, 619 | ⊢  | |
| : , : , : , : | ||||
| 307 | instantiation | 508, 509 | ⊢  | |
| : , : , : | ||||
| 308 | instantiation | 584, 351, 378 | ⊢  | |
: , :  , : | ||||
| 309 | instantiation | 584, 352, 353 | ⊢  | |
| : , : , : | ||||
| 310 | instantiation | 584, 354, 605 | ⊢  | |
| : , : , : | ||||
| 311 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 312 | instantiation | 685, 635, 355 | , ⊢ | |
| : , : , : | ||||
| 313 | instantiation | 508, 356 | ⊢  | |
:  , : , : | ||||
| 314 | conjecture | ⊢  | ||
| proveit.core_expr_types.tuples.extended_range_len | ||||
| 315 | instantiation | 357, 358 | ⊢  | |
| : , : , : | ||||
| 316 | instantiation | 584, 359, 360 | ⊢  | |
:  , :  , : | ||||
| 317 | instantiation | 578, 536, 361 | ⊢  | |
| : , : , : | ||||
| 318 | instantiation | 584, 362, 363 | ⊢  | |
: , :  , : | ||||
| 319 | conjecture | ⊢  | ||
| proveit.numbers.addition.subtraction.add_cancel_triple_12 | ||||
| 320 | conjecture | ⊢  | ||
| proveit.numbers.addition.subtraction.add_cancel_general | ||||
| 321 | instantiation | 685, 543, 364 | ⊢  | |
| : , : , : | ||||
| 322 | instantiation | 584, 365, 366 | ⊢  | |
: , :  , : | ||||
| 323 | conjecture | ⊢  | ||
| proveit.numbers.ordering.transitivity_less_less_eq | ||||
| 324 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.less_0_1 | ||||
| 325 | instantiation | 367, 633, 368, 369, 370, 371* | , ⊢  | |
| : , : , : | ||||
| 326 | instantiation | 372, 607, 634, 630, 373, 374* | ⊢  | |
| : , : , : | ||||
| 327 | instantiation | 584, 375, 376 | , ⊢  | |
: , :  , : | ||||
| 328 | conjecture | ⊢  | ||
| proveit.core_expr_types.tuples.general_len | ||||
| 329 | instantiation | 631 | ⊢  | |
: , :  | ||||
| 330 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 331 | instantiation | 526, 610, 425 | ⊢  | |
| : , : , : | ||||
| 332 | instantiation | 584, 377, 378 | ⊢  | |
:  , : , : | ||||
| 333 | instantiation | 584, 379, 380 | ⊢  | |
: , :  , : | ||||
| 334 | conjecture | ⊢  | ||
| proveit.linear_algebra.tensors.tensor_prod_disassociation | ||||
| 335 | instantiation | 431, 666, 381, 382, 383 | ⊢  | |
| : , : , : | ||||
| 336 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 337 | instantiation | 384, 432, 528, 433, 434, 385, 386 | ⊢  | |
: , : , :  , : | ||||
| 338 | axiom | ⊢  | ||
| proveit.physics.quantum.QPE._u_ket_register | ||||
| 339 | instantiation | 685, 655, 670 | , ⊢  | |
| : , : , : | ||||
| 340 | instantiation | 675, 680, 656 | ⊢  | |
| : , : | ||||
| 341 | assumption | ⊢ | ||
| 342 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 343 | instantiation | 584, 387, 388 | ⊢  | |
:  , :  , : | ||||
| 344 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 345 | instantiation | 584, 389, 603 | ⊢  | |
:  , :  , : | ||||
| 346 | instantiation | 591, 592, 390, 602, 594, 595, 391, 597 | ⊢  | |
:  , :  | ||||
| 347 | instantiation | 685, 551, 392 | , ⊢  | |
| : , : , : | ||||
| 348 | instantiation | 406, 689, 666 | ⊢  | |
| : , : | ||||
| 349 | instantiation | 576, 407 | ⊢  | |
:  , : , : | ||||
| 350 | instantiation | 584, 393, 394 | ⊢  | |
: , :  , : | ||||
| 351 | instantiation | 584, 395, 396 | ⊢  | |
: , :  , : | ||||
| 352 | instantiation | 576, 399 | ⊢  | |
: , :  , : | ||||
| 353 | instantiation | 584, 397, 398 | ⊢  | |
: , :  , : | ||||
| 354 | instantiation | 576, 399 | ⊢  | |
| : , : , : | ||||
| 355 | instantiation | 685, 652, 400 | , ⊢ | |
| : , : , : | ||||
| 356 | instantiation | 526, 527, 401 | ⊢  | |
| : , : , : | ||||
| 357 | conjecture | ⊢  | ||
| proveit.core_expr_types.tuples.range_len_is_nat | ||||
| 358 | instantiation | 526, 536, 426 | ⊢  | |
| : , : , : | ||||
| 359 | instantiation | 576, 488 | ⊢  | |
:  , :  , :  | ||||
| 360 | instantiation | 584, 402, 403 | ⊢  | |
: , :  , : | ||||
| 361 | instantiation | 606, 617, 618 | ⊢  | |
| : , : | ||||
| 362 | instantiation | 576, 488 | ⊢  | |
:  , : , : | ||||
| 363 | instantiation | 584, 404, 405 | ⊢  | |
: , :  , : | ||||
| 364 | instantiation | 406, 689, 687 | ⊢  | |
| : , : | ||||
| 365 | instantiation | 576, 407 | ⊢  | |
:  , : , : | ||||
| 366 | instantiation | 613, 610, 617, 619 | ⊢  | |
| : , : , : , : | ||||
| 367 | conjecture | ⊢  | ||
| proveit.numbers.addition.weak_bound_via_left_term_bound | ||||
| 368 | instantiation | 685, 652, 408 | ⊢  | |
| : , : , : | ||||
| 369 | instantiation | 685, 652, 409 | , ⊢  | |
| : , : , : | ||||
| 370 | instantiation | 410, 676, 677, 483 | , ⊢  | |
| : , : , : | ||||
| 371 | instantiation | 584, 411, 412 | ⊢  | |
: , :  , : | ||||
| 372 | conjecture | ⊢  | ||
| proveit.numbers.ordering.less_eq_shift_add_right | ||||
| 373 | instantiation | 413, 634, 649, 633, 573, 414, 415*, 416* | ⊢  | |
| : , : , : | ||||
| 374 | instantiation | 578, 417, 418 | ⊢  | |
:  , :  , :  | ||||
| 375 | instantiation | 609, 682, 614, 610, 615, 419, 421, 618, 617, 619 | , ⊢  | |
: , : , : , : , :  , : | ||||
| 376 | instantiation | 420, 610, 682, 615, 421, 619, 617 | , ⊢  | |
: , : , : , :  , : , : , : | ||||
| 377 | instantiation | 422, 664, 423, 424, 425, 426 | ⊢  | |
: ,  :  , :  , :  | ||||
| 378 | instantiation | 584, 427, 428 | ⊢  | |
: , :  , : | ||||
| 379 | instantiation | 576, 562 | ⊢  | |
| : , : , : | ||||
| 380 | instantiation | 584, 429, 430 | ⊢  | |
: , :  , : | ||||
| 381 | instantiation | 631 | ⊢  | |
:  , :  | ||||
| 382 | instantiation | 431, 432, 528, 433, 434 | ⊢  | |
| : , : , : | ||||
| 383 | instantiation | 550, 435 | ⊢  | |
| : | ||||
| 384 | conjecture | ⊢  | ||
| proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space | ||||
| 385 | instantiation | 584, 436, 467 | ⊢  | |
:  , : , : | ||||
| 386 | modus ponens | 437, 438 | ⊢  | |
| 387 | instantiation | 576, 439 | ⊢  | |
:  , : , : | ||||
| 388 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.add_2_1 | ||||
| 389 | instantiation | 576, 440 | ⊢  | |
: , :  , : | ||||
| 390 | instantiation | 624 | ⊢  | |
: , : , : , :  ,  : | ||||
| 391 | instantiation | 685, 635, 441 | ⊢  | |
| : , : , : | ||||
| 392 | instantiation | 568, 569, 442 | , ⊢  | |
: , :  | ||||
| 393 | instantiation | 584, 443, 444 | ⊢  | |
: , :  , : | ||||
| 394 | instantiation | 540, 610, 664, 682, 445, 615, 617, 619, 603* | ⊢  | |
| : , : , : , : , : , : | ||||
| 395 | instantiation | 576, 605 | ⊢  | |
:  , : , : | ||||
| 396 | instantiation | 576, 562 | ⊢  | |
| : , : , : | ||||
| 397 | instantiation | 609, 682, 664, 610, 615, 454, 582, 619 | ⊢  | |
: , : , : , : , :  , : | ||||
| 398 | instantiation | 540, 610, 664, 682, 445, 615, 582, 619, 603* | ⊢  | |
: , : , : , :  , : , : | ||||
| 399 | instantiation | 608, 619 | ⊢  | |
| : | ||||
| 400 | instantiation | 685, 655, 446 | , ⊢ | |
| : , : , : | ||||
| 401 | instantiation | 584, 447, 448 | ⊢  | |
: , :  , : | ||||
| 402 | instantiation | 584, 449, 450 | ⊢  | |
: , :  , : | ||||
| 403 | instantiation | 587, 602, 617 | ⊢  | |
| : , : | ||||
| 404 | instantiation | 584, 451, 452 | ⊢  | |
: , :  , : | ||||
| 405 | instantiation | 540, 682, 664, 610, 615, 541, 619, 559, 617, 577* | ⊢  | |
: , : , : , : , :  , : | ||||
| 406 | conjecture | ⊢  | ||
| proveit.numbers.addition.add_nat_pos_closure_bin | ||||
| 407 | conjecture | ⊢  | ||
| proveit.numbers.negation.negated_zero | ||||
| 408 | instantiation | 685, 655, 676 | ⊢  | |
| : , : , : | ||||
| 409 | instantiation | 685, 655, 453 | , ⊢  | |
| : , : , : | ||||
| 410 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.integers.interval_lower_bound | ||||
| 411 | instantiation | 609, 682, 664, 610, 615, 454, 582, 619, 617 | ⊢  | |
| : , : , : , : , : , : | ||||
| 412 | instantiation | 455, 617, 619 | ⊢  | |
| : , : | ||||
| 413 | conjecture | ⊢  | ||
| proveit.numbers.multiplication.reversed_weak_bound_via_right_factor_bound | ||||
| 414 | instantiation | 511, 456 | ⊢  | |
| : , : | ||||
| 415 | instantiation | 458, 619, 617, 457* | ⊢  | |
| : , : | ||||
| 416 | instantiation | 458, 619, 459* | ⊢  | |
| : , : | ||||
| 417 | instantiation | 604, 619, 602, 603 | ⊢  | |
| : , : , : | ||||
| 418 | instantiation | 606, 602, 618 | ⊢  | |
| : , : | ||||
| 419 | instantiation | 632 | ⊢  | |
| : , : , : | ||||
| 420 | conjecture | ⊢  | ||
| proveit.numbers.addition.subtraction.add_cancel_general_rev | ||||
| 421 | instantiation | 685, 635, 460 | , ⊢  | |
| : , : , : | ||||
| 422 | axiom | ⊢  | ||
| proveit.core_expr_types.operations.operands_substitution | ||||
| 423 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 424 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 425 | instantiation | 540, 682, 664, 610, 615, 461, 619, 618, 462* | ⊢  | |
: , : , : , : , :  , : | ||||
| 426 | instantiation | 584, 463, 464 | ⊢  | |
: , :  , : | ||||
| 427 | instantiation | 609, 610, 664, 682, 611, 615, 619, 617, 618 | ⊢  | |
| : , : , : , : , : , : | ||||
| 428 | instantiation | 465, 619, 617 | ⊢  | |
| : , : | ||||
| 429 | instantiation | 609, 610, 664, 682, 611, 615, 612, 617, 618 | ⊢  | |
| : , : , : , : , : , : | ||||
| 430 | instantiation | 613, 682, 664, 615, 611, 617, 618 | ⊢  | |
| : , : , : , : | ||||
| 431 | conjecture | ⊢  | ||
| proveit.linear_algebra.tensors.tensor_prod_of_vec_spaces_is_vec_space | ||||
| 432 | instantiation | 526, 689, 528 | ⊢  | |
:  , : , : | ||||
| 433 | instantiation | 584, 466, 467 | ⊢  | |
:  , : , : | ||||
| 434 | instantiation | 468, 676, 677, 533, 472 | ⊢  | |
: , : , :  | ||||
| 435 | instantiation | 663, 664, 469 | ⊢  | |
| : , : | ||||
| 436 | instantiation | 578, 470, 528 | ⊢  | |
:  , : , : | ||||
| 437 | instantiation | 471, 676, 677, 472 | ⊢  | |
| : , : , : , : | ||||
| 438 | generalization | 473 | ⊢  | |
| 439 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.add_2_0 | ||||
| 440 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.add_1_0 | ||||
| 441 | instantiation | 685, 652, 474 | ⊢  | |
| : , : , : | ||||
| 442 | instantiation | 591, 592, 593, 602, 594, 595, 475, 597 | , ⊢  | |
: , :  | ||||
| 443 | instantiation | 609, 682, 664, 615, 477, 476, 617, 619, 612 | ⊢  | |
: , : , : , : , : , :  | ||||
| 444 | instantiation | 613, 664, 610, 477, 617, 619 | ⊢  | |
| : , : , : , : | ||||
| 445 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 446 | instantiation | 685, 478, 479 | , ⊢ | |
:  , : , : | ||||
| 447 | instantiation | 576, 488 | ⊢  | |
| : , : , : | ||||
| 448 | instantiation | 584, 480, 481 | ⊢  | |
| : , : , : | ||||
| 449 | instantiation | 609, 610, 664, 557, 612, 617, 559, 602 | ⊢  | |
: , : , : , : , :  , :  | ||||
| 450 | instantiation | 613, 682, 614, 615, 482, 617, 559, 602 | ⊢  | |
: , : , : , :  | ||||
| 451 | instantiation | 609, 610, 664, 682, 557, 615, 619, 617, 559 | ⊢  | |
| : , : , : , : , : , : | ||||
| 452 | instantiation | 558, 610, 682, 615, 619, 617, 559 | ⊢  | |
: , : , : , : , : , :  , : | ||||
| 453 | instantiation | 685, 672, 483 | , ⊢  | |
| : , : , : | ||||
| 454 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 455 | conjecture | ⊢  | ||
| proveit.numbers.addition.subtraction.add_cancel_triple_31 | ||||
| 456 | instantiation | 546, 598 | ⊢  | |
| : | ||||
| 457 | instantiation | 484, 617 | ⊢  | |
| : | ||||
| 458 | conjecture | ⊢  | ||
| proveit.numbers.multiplication.mult_neg_left | ||||
| 459 | instantiation | 485, 619 | ⊢  | |
| : | ||||
| 460 | instantiation | 685, 652, 486 | , ⊢ | |
| : , : , : | ||||
| 461 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 462 | instantiation | 584, 487, 605 | ⊢  | |
:  , : , : | ||||
| 463 | instantiation | 576, 488 | ⊢  | |
:  , : , : | ||||
| 464 | instantiation | 584, 489, 490 | ⊢  | |
: , :  , : | ||||
| 465 | conjecture | ⊢  | ||
| proveit.numbers.addition.subtraction.add_cancel_triple_13 | ||||
| 466 | instantiation | 578, 491, 528 | ⊢  | |
:  , : , : | ||||
| 467 | instantiation | 492, 493 | ⊢  | |
| : , : | ||||
| 468 | conjecture | ⊢  | ||
| proveit.logic.booleans.conjunction.redundant_conjunction_general | ||||
| 469 | instantiation | 685, 543, 494 | ⊢  | |
| : , : , : | ||||
| 470 | instantiation | 508, 509 | ⊢  | |
 :  , : , : | ||||
| 471 | conjecture | ⊢  | ||
| proveit.logic.booleans.conjunction.conjunction_from_quantification | ||||
| 472 | instantiation | 526, 495, 605 | ⊢  | |
| : , : , : | ||||
| 473 | instantiation | 532, 533, 496, 497 | , ⊢ | |
| : , : , : , : | ||||
| 474 | instantiation | 685, 655, 498 | ⊢  | |
| : , : , : | ||||
| 475 | instantiation | 685, 635, 499 | , ⊢  | |
: , : , :  | ||||
| 476 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 477 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 478 | instantiation | 675, 654, 680 | ⊢  | |
| : , : | ||||
| 479 | assumption | ⊢ | ||
| 480 | instantiation | 584, 500, 501 | ⊢  | |
: , :  , : | ||||
| 481 | instantiation | 502, 617 | ⊢  | |
| : | ||||
| 482 | instantiation | 632 | ⊢  | |
| : , : , : | ||||
| 483 | assumption | ⊢ | ||
| 484 | conjecture | ⊢  | ||
| proveit.numbers.multiplication.elim_one_left | ||||
| 485 | conjecture | ⊢  | ||
| proveit.numbers.multiplication.elim_one_right | ||||
| 486 | instantiation | 685, 655, 503 | , ⊢ | |
| : , : , : | ||||
| 487 | instantiation | 576, 579 | ⊢  | |
: , :  , : | ||||
| 488 | instantiation | 581, 582, 602, 583* | ⊢  | |
| : , : | ||||
| 489 | instantiation | 584, 504, 505 | ⊢  | |
: , :  , : | ||||
| 490 | instantiation | 540, 610, 664, 682, 506, 615, 617, 559, 619, 507* | ⊢  | |
: , : , : , : , :  , : | ||||
| 491 | instantiation | 508, 509 | ⊢  | |
| : , : , : | ||||
| 492 | theorem | ⊢  | ||
| proveit.logic.equality.equals_reversal | ||||
| 493 | instantiation | 510, 527 | ⊢  | |
| : , : | ||||
| 494 | axiom | ⊢  | ||
| proveit.physics.quantum.QPE._s_in_nat_pos | ||||
| 495 | instantiation | 511, 512 | ⊢  | |
| : , : | ||||
| 496 | instantiation | 685, 635, 513 | ⊢  | |
| : , : , : | ||||
| 497 | instantiation | 514, 533, 515, 516 | , ⊢ | |
| : , : , : , : | ||||
| 498 | instantiation | 685, 686, 517 | ⊢  | |
| : , : , : | ||||
| 499 | instantiation | 685, 652, 518 | , ⊢  | |
| : , : , : | ||||
| 500 | instantiation | 584, 519, 520 | ⊢  | |
: , :  , : | ||||
| 501 | instantiation | 540, 682, 614, 610, 615, 521, 619, 559, 617, 522* | ⊢  | |
: , : , : , : , :  , : | ||||
| 502 | conjecture | ⊢  | ||
| proveit.numbers.addition.elim_zero_left | ||||
| 503 | instantiation | 685, 644, 523 | , ⊢ | |
:  , : , : | ||||
| 504 | instantiation | 609, 610, 664, 557, 612, 617, 559, 619 | ⊢  | |
| : , : , : , : , : , : | ||||
| 505 | instantiation | 613, 682, 614, 615, 524, 617, 559, 619 | ⊢  | |
: , : , : , :  | ||||
| 506 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 507 | instantiation | 578, 577, 525 | ⊢  | |
:  , :  , :  | ||||
| 508 | conjecture | ⊢  | ||
| proveit.core_expr_types.tuples.range_len | ||||
| 509 | instantiation | 526, 527, 528 | ⊢  | |
| : , : , : | ||||
| 510 | conjecture | ⊢  | ||
| proveit.core_expr_types.tuples.range_from1_len | ||||
| 511 | conjecture | ⊢  | ||
| proveit.numbers.ordering.relax_less | ||||
| 512 | instantiation | 529, 607, 642, 649, 530, 605* | ⊢  | |
| : , : , : | ||||
| 513 | instantiation | 685, 638, 531 | ⊢  | |
:  , : , : | ||||
| 514 | conjecture | ⊢  | ||
| proveit.linear_algebra.addition.binary_closure | ||||
| 515 | conjecture | ⊢  | ||
| proveit.physics.quantum.algebra.ket_zero_in_qubit_space | ||||
| 516 | instantiation | 532, 533, 534, 535 | , ⊢ | |
| : , : , : , : | ||||
| 517 | instantiation | 663, 664, 536 | ⊢  | |
| : , : | ||||
| 518 | instantiation | 685, 655, 537 | , ⊢  | |
| : , : , : | ||||
| 519 | instantiation | 584, 538, 539 | ⊢  | |
: , :  , : | ||||
| 520 | instantiation | 558, 664, 610, 682, 541, 615, 619, 559, 617 | ⊢  | |
| : , : , : , : , : , : , : | ||||
| 521 | instantiation | 632 | ⊢  | |
| : , : , : | ||||
| 522 | instantiation | 540, 682, 664, 610, 615, 541, 619, 559, 542* | ⊢  | |
| : , : , : , : , : , : | ||||
| 523 | assumption | ⊢ | ||
| 524 | instantiation | 632 | ⊢  | |
| : , : , : | ||||
| 525 | instantiation | 606, 619, 559 | ⊢  | |
| : , : | ||||
| 526 | theorem | ⊢  | ||
| proveit.logic.equality.sub_left_side_into | ||||
| 527 | instantiation | 685, 543, 689 | ⊢  | |
| : , : , : | ||||
| 528 | instantiation | 584, 544, 545 | ⊢  | |
: , :  , : | ||||
| 529 | conjecture | ⊢  | ||
| proveit.numbers.ordering.less_shift_add_right | ||||
| 530 | instantiation | 546, 684 | ⊢  | |
| : | ||||
| 531 | instantiation | 547, 548, 588, 549 | ⊢  | |
: , :  | ||||
| 532 | conjecture | ⊢  | ||
| proveit.linear_algebra.scalar_multiplication.scalar_mult_closure | ||||
| 533 | instantiation | 550, 666 | ⊢ | |
| : | ||||
| 534 | instantiation | 685, 551, 552 | , ⊢ | |
| : , : , : | ||||
| 535 | conjecture | ⊢  | ||
| proveit.physics.quantum.algebra.ket_one_in_qubit_space | ||||
| 536 | instantiation | 553, 554, 555 | ⊢ | |
| : | ||||
| 537 | instantiation | 685, 686, 556 | , ⊢  | |
| : , : , : | ||||
| 538 | instantiation | 609, 610, 664, 557, 619, 617, 559 | ⊢  | |
| : , : , : , : , : , : | ||||
| 539 | instantiation | 558, 610, 619, 617, 559 | ⊢  | |
| : , : , : , : , : , : , : | ||||
| 540 | conjecture | ⊢  | ||
| proveit.numbers.addition.association | ||||
| 541 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 542 | instantiation | 584, 560, 561 | ⊢  | |
:  , :  , : | ||||
| 543 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat | ||||
| 544 | instantiation | 576, 562 | ⊢  | |
| : , : , : | ||||
| 545 | instantiation | 584, 563, 564 | ⊢  | |
: , :  , : | ||||
| 546 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.integers.negative_if_in_neg_int | ||||
| 547 | conjecture | ⊢  | ||
| proveit.numbers.division.div_real_pos_closure | ||||
| 548 | instantiation | 685, 636, 565 | ⊢  | |
:  , : , : | ||||
| 549 | instantiation | 566, 567 | ⊢  | |
| : | ||||
| 550 | conjecture | ⊢  | ||
| proveit.linear_algebra.complex_vec_set_is_vec_space | ||||
| 551 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.complex_numbers.complex_nonzero_within_complex | ||||
| 552 | instantiation | 568, 569, 570 | , ⊢ | |
| : , : | ||||
| 553 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.integers.nonneg_int_is_natural | ||||
| 554 | instantiation | 678, 656, 571 | ⊢  | |
| : , : | ||||
| 555 | instantiation | 572, 573 | ⊢  | |
| : , : | ||||
| 556 | instantiation | 663, 664, 574 | , ⊢  | |
: , :  | ||||
| 557 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 558 | conjecture | ⊢  | ||
| proveit.numbers.addition.leftward_commutation | ||||
| 559 | instantiation | 685, 635, 575 | ⊢  | |
| : , : , : | ||||
| 560 | instantiation | 576, 577 | ⊢  | |
| : , : , : | ||||
| 561 | instantiation | 578, 579, 580 | ⊢  | |
:  , : , : | ||||
| 562 | instantiation | 581, 582, 619, 583* | ⊢  | |
| : , : | ||||
| 563 | instantiation | 584, 585, 586 | ⊢  | |
: , :  , : | ||||
| 564 | instantiation | 587, 619, 617 | ⊢  | |
| : , : | ||||
| 565 | instantiation | 685, 650, 687 | ⊢  | |
| : , : , : | ||||
| 566 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero | ||||
| 567 | instantiation | 685, 622, 588 | ⊢  | |
: , :  , : | ||||
| 568 | conjecture | ⊢  | ||
| proveit.numbers.exponentiation.exp_complex_nonzero_closure | ||||
| 569 | instantiation | 685, 589, 590 | ⊢  | |
| : , : , : | ||||
| 570 | instantiation | 591, 592, 593, 602, 594, 595, 596, 597 | , ⊢ | |
| : , : | ||||
| 571 | instantiation | 685, 683, 598 | ⊢  | |
:  , : , : | ||||
| 572 | conjecture | ⊢  | ||
| proveit.numbers.addition.subtraction.nonneg_difference | ||||
| 573 | instantiation | 599, 689 | ⊢ | |
| : | ||||
| 574 | instantiation | 667, 600 | , ⊢  | |
| : | ||||
| 575 | instantiation | 648, 630 | ⊢  | |
| : | ||||
| 576 | axiom | ⊢  | ||
| proveit.logic.equality.substitution | ||||
| 577 | instantiation | 601, 619, 602, 603 | ⊢  | |
| : , : , : | ||||
| 578 | theorem | ⊢  | ||
| proveit.logic.equality.sub_right_side_into | ||||
| 579 | instantiation | 604, 612, 619, 605 | ⊢  | |
| : , : , : | ||||
| 580 | instantiation | 606, 619, 618 | ⊢  | |
| : , : | ||||
| 581 | conjecture | ⊢  | ||
| proveit.numbers.negation.distribute_neg_through_binary_sum | ||||
| 582 | instantiation | 685, 635, 607 | ⊢  | |
| : , : , : | ||||
| 583 | instantiation | 608, 617 | ⊢  | |
| : | ||||
| 584 | axiom | ⊢  | ||
| proveit.logic.equality.equals_transitivity | ||||
| 585 | instantiation | 609, 610, 664, 611, 612, 617, 618, 619 | ⊢  | |
| : , : , : , : , : , : | ||||
| 586 | instantiation | 613, 682, 614, 615, 616, 617, 618, 619 | ⊢  | |
: , : , : , :  | ||||
| 587 | conjecture | ⊢  | ||
| proveit.numbers.addition.subtraction.add_cancel_triple_32 | ||||
| 588 | instantiation | 620, 621 | ⊢  | |
| : | ||||
| 589 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero | ||||
| 590 | instantiation | 685, 622, 623 | ⊢  | |
| : , : , : | ||||
| 591 | conjecture | ⊢  | ||
| proveit.numbers.multiplication.mult_complex_closure | ||||
| 592 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.nat5 | ||||
| 593 | instantiation | 624 | ⊢  | |
| : , : , : , : , : | ||||
| 594 | instantiation | 685, 635, 625 | ⊢  | |
| : , : , : | ||||
| 595 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.complex_numbers.i_is_complex | ||||
| 596 | instantiation | 685, 635, 626 | , ⊢ | |
| : , : , : | ||||
| 597 | instantiation | 685, 635, 627 | ⊢  | |
| : , : , : | ||||
| 598 | instantiation | 688, 687 | ⊢  | |
| : | ||||
| 599 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound | ||||
| 600 | instantiation | 669, 628, 629 | , ⊢  | |
| : | ||||
| 601 | conjecture | ⊢  | ||
| proveit.numbers.addition.subtraction.subtract_from_add_reversed | ||||
| 602 | instantiation | 685, 635, 630 | ⊢  | |
| : , : , : | ||||
| 603 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.add_1_1 | ||||
| 604 | conjecture | ⊢  | ||
| proveit.numbers.addition.subtraction.subtract_from_add | ||||
| 605 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.add_0_1 | ||||
| 606 | conjecture | ⊢  | ||
| proveit.numbers.addition.commutation | ||||
| 607 | instantiation | 648, 633 | ⊢  | |
| : | ||||
| 608 | conjecture | ⊢  | ||
| proveit.numbers.negation.double_negation | ||||
| 609 | conjecture | ⊢  | ||
| proveit.numbers.addition.disassociation | ||||
| 610 | theorem | ⊢  | ||
| proveit.numbers.numerals.decimals.nat1 | ||||
| 611 | instantiation | 631 | ⊢  | |
| : , : | ||||
| 612 | instantiation | 685, 635, 642 | ⊢  | |
| : , : , : | ||||
| 613 | conjecture | ⊢  | ||
| proveit.numbers.addition.elim_zero_any | ||||
| 614 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.nat3 | ||||
| 615 | conjecture | ⊢  | ||
| proveit.core_expr_types.tuples.tuple_len_0_typical_eq | ||||
| 616 | instantiation | 632 | ⊢  | |
| : , : , : | ||||
| 617 | instantiation | 685, 635, 633 | ⊢  | |
| : , : , : | ||||
| 618 | instantiation | 685, 635, 634 | ⊢  | |
| : , : , : | ||||
| 619 | instantiation | 685, 635, 649 | ⊢  | |
| : , : , : | ||||
| 620 | conjecture | ⊢  | ||
| proveit.numbers.exponentiation.sqrt_real_pos_closure | ||||
| 621 | instantiation | 685, 636, 637 | ⊢  | |
| : , : , : | ||||
| 622 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero | ||||
| 623 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.real_numbers.e_is_real_pos | ||||
| 624 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.tuple_len_5_typical_eq | ||||
| 625 | instantiation | 685, 638, 639 | ⊢  | |
| : , : , : | ||||
| 626 | instantiation | 685, 652, 640 | , ⊢ | |
| : , : , : | ||||
| 627 | instantiation | 641, 642, 649, 643 | ⊢  | |
| : , : , : | ||||
| 628 | instantiation | 685, 644, 645 | , ⊢  | |
| : , : , : | ||||
| 629 | instantiation | 673, 654, 677, 645 | , ⊢  | |
| : , : , : | ||||
| 630 | instantiation | 685, 652, 646 | ⊢  | |
| : , : , : | ||||
| 631 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.tuple_len_2_typical_eq | ||||
| 632 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.tuple_len_3_typical_eq | ||||
| 633 | instantiation | 685, 652, 647 | ⊢  | |
| : , : , : | ||||
| 634 | instantiation | 648, 649 | ⊢  | |
| : | ||||
| 635 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.complex_numbers.real_within_complex | ||||
| 636 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos | ||||
| 637 | instantiation | 685, 650, 666 | ⊢  | |
| : , : , : | ||||
| 638 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.real_numbers.real_pos_within_real | ||||
| 639 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.real_numbers.pi_is_real_pos | ||||
| 640 | instantiation | 685, 655, 651 | , ⊢ | |
| : , : , : | ||||
| 641 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real | ||||
| 642 | instantiation | 685, 652, 653 | ⊢  | |
| : , : , : | ||||
| 643 | axiom | ⊢  | ||
| proveit.physics.quantum.QPE._phase_in_interval | ||||
| 644 | instantiation | 675, 654, 677 | ⊢  | |
| : , : | ||||
| 645 | assumption | ⊢ | ||
| 646 | instantiation | 685, 655, 660 | ⊢  | |
| : , : , : | ||||
| 647 | instantiation | 685, 655, 656 | ⊢  | |
| : , : , : | ||||
| 648 | conjecture | ⊢  | ||
| proveit.numbers.negation.real_closure | ||||
| 649 | instantiation | 657, 658, 687 | ⊢  | |
| : , : , : | ||||
| 650 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos | ||||
| 651 | instantiation | 685, 686, 659 | , ⊢ | |
| : , : , : | ||||
| 652 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.real_numbers.rational_within_real | ||||
| 653 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.rational_numbers.zero_is_rational | ||||
| 654 | instantiation | 678, 679, 660 | ⊢  | |
| : , : | ||||
| 655 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.rational_numbers.int_within_rational | ||||
| 656 | instantiation | 685, 686, 689 | ⊢  | |
| : , : , : | ||||
| 657 | theorem | ⊢  | ||
| proveit.logic.sets.inclusion.unfold_subset_eq | ||||
| 658 | instantiation | 661, 662 | ⊢  | |
| : , : | ||||
| 659 | instantiation | 663, 664, 665 | , ⊢ | |
| : , : | ||||
| 660 | instantiation | 685, 686, 666 | ⊢  | |
| : , : , : | ||||
| 661 | theorem | ⊢  | ||
| proveit.logic.sets.inclusion.relax_proper_subset | ||||
| 662 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.real_numbers.nat_pos_within_real | ||||
| 663 | conjecture | ⊢  | ||
| proveit.numbers.exponentiation.exp_natpos_closure | ||||
| 664 | theorem | ⊢  | ||
| proveit.numbers.numerals.decimals.nat2 | ||||
| 665 | instantiation | 667, 668 | , ⊢ | |
| : | ||||
| 666 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.posnat2 | ||||
| 667 | conjecture | ⊢  | ||
| proveit.numbers.negation.nat_closure | ||||
| 668 | instantiation | 669, 670, 671 | , ⊢ | |
| : | ||||
| 669 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.integers.nonpos_int_is_int_nonpos | ||||
| 670 | instantiation | 685, 672, 674 | , ⊢ | |
| : , : , : | ||||
| 671 | instantiation | 673, 676, 677, 674 | , ⊢ | |
| : , : , : | ||||
| 672 | instantiation | 675, 676, 677 | ⊢  | |
| : , : | ||||
| 673 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.integers.interval_upper_bound | ||||
| 674 | assumption | ⊢ | ||
| 675 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.integers.int_interval_within_int | ||||
| 676 | instantiation | 678, 679, 680 | ⊢  | |
| : , : | ||||
| 677 | instantiation | 685, 681, 682 | ⊢  | |
| : , : , : | ||||
| 678 | conjecture | ⊢  | ||
| proveit.numbers.addition.add_int_closure_bin | ||||
| 679 | instantiation | 685, 683, 684 | ⊢  | |
| : , : , : | ||||
| 680 | instantiation | 685, 686, 687 | ⊢  | |
| : , : , : | ||||
| 681 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.integers.nat_within_int | ||||
| 682 | axiom | ⊢  | ||
| proveit.numbers.number_sets.natural_numbers.zero_in_nats | ||||
| 683 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.integers.neg_int_within_int | ||||
| 684 | instantiation | 688, 689 | ⊢  | |
| : | ||||
| 685 | theorem | ⊢  | ||
| proveit.logic.sets.inclusion.superset_membership_from_proper_subset | ||||
| 686 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.integers.nat_pos_within_int | ||||
| 687 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.posnat1 | ||||
| 688 | conjecture | ⊢  | ||
| proveit.numbers.negation.int_neg_closure | ||||
| 689 | assumption | ⊢ | ||
| *equality replacement requirements | ||||